Linear Search
Linear Search is often used in many application. What Linear Search does is going through very element in the medium until it found the right element. The implementation is:
|[ Var x : Int;
{ Precondition: The thing you are search must be searchable in the medium }
{ We are searching for the smallest x for which b.x, a boolean expression, holds and x must be bigger than 0 }
x : = 0;
do NOT( b.x ) -> x := x + 1 od
{ Postcondition: x is the smallest integer number for which b.x holds }
]|
This implementation shouldn't be a big problem for you. I think everyone has made a search algorithm like one. So that is why I haven't provided this algorithm with a huge explanation.
Here is an example how to use this algorithm:
What we want to find is the minimal x for which (x*x) >= N
{ Note: '<=' Means Bigger or Equal this is not an arrow!! And 'N' is a random number which is bigger than 0 }
What we are searching for is the square of N rounded above. And we know that what we are searching for is
searchable if N is bigger than 0.
Thus b.x is the same as: (x*x) >= N
And Not( b.x ) is the same as (x*x) < N
If you substitute this information into the implementation of Linear Search you have made a program which works.
|[ Var x : Int;
{ Precondition: N >= 0 and The element what you're searching for is searchable }
x : = 0;
Do (x*x) < N -> x : = x + 1 Od
{ The smallest ( x >= 0 ) for which (x*x) >= N holds }
]|
The complexity of this program is N. Notation is : O(N). Which means that you have to go through this loop N times before you find what you are looking for. With the Binary Search you can reduce the complexity to O( Log(N) ). Which is ofcourse a lot faster.